package Automaton;

import java.io.PrintWriter;
import java.util.*;

import Patterns.Pattern;

import main.*;

public class MembershipSolver implements Interruptible 
{
	//This class solves instances of the membership problem by using a Janus automaton
	private PrintWriter writer;
	private int[] nextMapping;
	private int[] counterMapping;
	private int[] roMapping;
	private int[][] gaps;
	private ArrayList<Pattern> patternList;
	ArrayList<String> wordList;
	private Pattern pattern;
	private String word;
	private boolean isMember;
	private int[] counterBounds;
	private boolean interrupted = false;

	public boolean isInterrupted() {
		return interrupted;
	}

	public void interrupt() {
		interrupted = true;
	}

	public void setInterrupted(boolean interrupted) {
		this.interrupted = interrupted;
	}

	public boolean isMember() {
		return isMember;
	}

	public MembershipSolver(int numberOfCounters) {
		counterBounds = new int[numberOfCounters];
	}

	public MembershipSolver() {

	}

	public synchronized void stop() {
		if (this != null) {
			this.stop();
		}
	}

	public void setInstance(Patterns.Pattern _pattern, String _word) {
		pattern = _pattern;
		word = _word;
	}

	private void computeMappings(Pattern pattern) 
	{
		nextMapping = new int[pattern.getLength()];
		int[] lastPositions = new int[pattern.getVarNumber()];

		//Compute the "next"-mapping (maps a pattern position to the next position with the same variable)
		for (int i = 0; i < nextMapping.length; i++) 
		{
			nextMapping[i] = -1;
		}

		for (int i = 0; i < lastPositions.length; i++) 
		{
			lastPositions[i] = -1;
		}

		for (int i = 0; i < pattern.getLength(); i++) 
		{
			int currentVariable = pattern.getVarOrder().get(i);
			if (lastPositions[currentVariable] == -1) 
			{
				lastPositions[currentVariable] = i;
			} 
			else 
			{
				nextMapping[lastPositions[currentVariable]] = i;
				lastPositions[currentVariable] = i;
			}
		}

		//Compute the "counter"-mapping (maps a variable to a counter of the Janus automaton)
		int counterNumber = pattern.getVarDistance() + 1;
		counterMapping = new int[pattern.getVarNumber()];
		boolean[] counterInUse = new boolean[counterNumber];
		boolean[] variableAllocated = new boolean[pattern.getVarNumber()];

		for (int i = 0; i < counterNumber; i++) 
		{
			counterInUse[i] = false;
		}

		for (int i = 0; i < pattern.getVarNumber(); i++) 
		{
			variableAllocated[i] = false;
		}

		for (int i = 0; i < pattern.getLength(); i++) 
		{
			if (nextMapping[i] == -1) 
			{
				counterInUse[counterMapping[pattern.getVarOrder().get(i)]] = false;
			} 
			else 
			{
				for (int j = i; j < nextMapping[i]; j++) 
				{
					if (!variableAllocated[pattern.getVarOrder().get(j)]) 
					{
						int freeCounter = -1;
						for (int k = 0; k < counterInUse.length; k++) 
						{
							if (!counterInUse[k]) 
							{
								freeCounter = k;
								break;
							}
						}
						counterMapping[pattern.getVarOrder().get(j)] = freeCounter;
						variableAllocated[pattern.getVarOrder().get(j)] = true;
						counterInUse[freeCounter] = true;
					}
				}
			}
		}

		//Compute the "ro"-mapping (maps a variable to its rightmost position in the pattern)
		int length = pattern.getLength();
		int varNumber = pattern.getVarNumber();
		roMapping = new int[varNumber];

		for (int i = 0; i < varNumber; i++) 
		{
			roMapping[i] = -1;
		}

		for (int i = 0; i < length; i++) 
		{
			roMapping[pattern.getVarOrder().get(i)] = i;
		}
	}

	private void computeGaps(Pattern pattern) 
	{
		//Computes the gaps, i.e. the parts the right input head has to be moved over in order to reach
		//the next matching position
		
		int l = 0;
		int r = 0;
		int length = pattern.getLength();
		gaps = new int[length][2];

		while (l < length) 
		{
			if (nextMapping[l] == -1) 
			{
				if (l == r) 
				{
					gaps[l][0] = r;
					gaps[l][1] = r + 1;
					l = l + 1;
					r = r + 1;
				} 
				else 
				{
					gaps[l][0] = -1;
					gaps[l][1] = -1;
					l = l + 1;
				}
			} 
			else 
			{
				gaps[l][0] = r;
				gaps[l][1] = nextMapping[l];
				r = nextMapping[l] + 1;
				l = l + 1;
			}
		}
	}

	public boolean solveInstance(Pattern pattern, String word) 
	{
		
		interrupted = false;

		//Compute the necessary mappings for solving the membership test 
		computeMappings(pattern);
		//Computes the "Gaps"
		computeGaps(pattern);

		//Create initial configuration and visit it
		Hashtable<String, Integer> confiVisited = new Hashtable<String, Integer>();
		confiVisited.put("INITIALCONF", 1);

		counterBounds = new int[pattern.getVarDistance() + 1];

		//search the computation graph for the final configuration
		boolean finalConfiFound = searchForFinalConfi("0", new int[pattern
				.getVarDistance() + 3], pattern.getVarOrder(), pattern
				.getOccurrenceVector(), word, confiVisited);

		return finalConfiFound;
	}

	private boolean searchForFinalConfi(String state, int[] headsCounters,
			ArrayList<Integer> varOrder, int[] occurrenceVector, String word,
			Hashtable<String, Integer> confiVisited) 
	{
		//Stop recursion, if test is interrupted
		if (interrupted) 
		{
			return false;
		}
		
		int counterNumber = headsCounters.length - 2;
		String newState;
		String[] splittedState;
		int leftHeadPosition;
		int[] gap;

		//Get state prefix of the current state
		int statePrefix = Integer.valueOf(state.substring(0, 1));

		//One case for each statePrefix
		//If prefix is "0", the Janus automaton is initialised, else:
			//1: Initial state (the next finding state is entered)
			//2: Matching state (the factors on the head positions are checked for equality.
					//if successful, the next finding state is entered)
			//3: Reseting state (a counter is used for a certain variable for the last time.
					//Thus, a new counter bound is guessed by reseting the corresponding counter)
			//4: Finding state (the left and right head is moved to the next matching position)
		switch (statePrefix) 
		{
		case 0: //The initialisation of the automaton
			//For every counter find out the first variable using that counter,
			//as these counters have to guess a counter bound
			int[] firstVariables = new int[counterNumber];
			for (int i = 0; i < firstVariables.length; i++) 
			{
				firstVariables[i] = -1;
			}
			for (int i = 0; i < counterMapping.length; i++) 
			{
				if (firstVariables[counterMapping[i]] == -1) 
				{
					firstVariables[counterMapping[i]] = i;
				}
			}

			//Compute the occurrence vector for these variables,
			//as the upper bound for a guessed counter bound depends on the number of
			//occurrences of the corresponding variable
			int[] firstVariablesOccurrenceVector = new int[counterNumber];
			for (int i = 0; i < firstVariablesOccurrenceVector.length; i++) 
			{
				firstVariablesOccurrenceVector[i] = occurrenceVector[firstVariables[i]];
			}

			//Create new configurations 
			if (createInitialConfigurations(word.length(),
					firstVariablesOccurrenceVector, varOrder, word,
					confiVisited)) 
			{
				return true;
			}
		case 1: // Initial state
			// create new configuration with a finding state
			newState = "4:" + varOrder.get(0) + ":0";
			headsCounters[0] = 0;
			headsCounters[1] = 0;

			//If this configuration has not been visited yet, visit it 
			if (confiVisited.get(confiToKey(newState, headsCounters)) == null) 
			{
				confiVisited.put(confiToKey(newState, headsCounters), 1);
				if (searchForFinalConfi(newState, headsCounters, varOrder,
						occurrenceVector, word, confiVisited)) 
				{
					return true;
				}
			}
			return false;
		case 2: // Matching state
			splittedState = state.split(":");
			int matchVariable = Integer.valueOf(splittedState[1]);
			leftHeadPosition = Integer.valueOf(splittedState[2]);
			int counterBound = headsCounters[counterMapping[matchVariable] + 2];
			if ((headsCounters[0] + counterBound <= word.length())
					&& (headsCounters[1] + counterBound <= word.length())) 
			{
				//match the factors
				if (word.substring(headsCounters[0],
						headsCounters[0] + counterBound).equals(
						word.substring(headsCounters[1], headsCounters[1]
								+ counterBound))) 
				{
					//if the factors equal, create a new finding configuration
					newState = "4:" + varOrder.get(leftHeadPosition + 1) + ":"
							+ (leftHeadPosition + 1);
					headsCounters[0] = headsCounters[0] + counterBound;
					headsCounters[1] = headsCounters[1] + counterBound;

					//If this configuration has not been visited yet, visit it
					if (confiVisited.get(confiToKey(newState, headsCounters)) == null) 
					{
						confiVisited
								.put(confiToKey(newState, headsCounters), 1);
						if (searchForFinalConfi(newState, headsCounters,
								varOrder, occurrenceVector, word, confiVisited)) 
						{
							return true;
						}
					}
				}
			}
			return false;
		case 3: // Reseting state
			splittedState = state.split(":");
			int lastOccurrenceVariable = Integer.valueOf(splittedState[1]);
			int position = roMapping[lastOccurrenceVariable];
			gap = gaps[position];
			int stepsNumber = headsCounters[counterMapping[lastOccurrenceVariable] + 2];

			// If we have reached the last variable
			if (position == varOrder.size() - 1) 
			{
				//Check if the last factor has the right length
				if (headsCounters[0]
						+ headsCounters[counterMapping[lastOccurrenceVariable] + 2] == word
						.length()) 
				{
					return true;
				}
			} 
			else 
			{
				int newLeftHeadPosition = headsCounters[0] + stepsNumber;
				// If only the left head has to be moved
				if ((gap[0] == -1) && (gap[1] == -1)
						&& (newLeftHeadPosition <= word.length())) 
				{
					//Compute the bound for the new counter bound to guess
					int upperBoundForNewCounterBound = computeBoundForNewCounterBound(
							varOrder, headsCounters.length - 3, word,
							newLeftHeadPosition, position, headsCounters);
					// For all possible new counter bounds, create a
					// Configuration
					for (int i = 0; i <= upperBoundForNewCounterBound; i++) 
					{
						if (interrupted) 
						{
							return false;
						}
						int[] newHeadsCounters = new int[headsCounters.length];
						newHeadsCounters = headsCounters.clone();
						newState = "4:" + varOrder.get(position + 1) + ":"
								+ (position + 1);
						newHeadsCounters[0] = newLeftHeadPosition;
						newHeadsCounters[counterMapping[lastOccurrenceVariable] + 2] = i;

						if (confiVisited.get(confiToKey(newState,
								newHeadsCounters)) == null) 
						{
							confiVisited.put(confiToKey(newState,
									newHeadsCounters), 1);
							if (searchForFinalConfi(newState, newHeadsCounters,
									varOrder, occurrenceVector, word,
									confiVisited)) 
							{
								return true;
							}
						}
					}
				}
				// If both, the left and right head have to be moved
				else if (newLeftHeadPosition <= word.length()) 
				{
					int upperBoundForNewCounterBound = computeBoundForNewCounterBound(
							varOrder, headsCounters.length - 3, word,
							newLeftHeadPosition, position, headsCounters);
					// For all possible new counter bounds, create a
					// Configuration
					for (int i = 0; i <= upperBoundForNewCounterBound; i++) 
					{
						if (interrupted) 
						{
							return false;
						}
						int[] newHeadsCounters = new int[headsCounters.length];
						newHeadsCounters = headsCounters.clone();
						newState = "4:" + varOrder.get(position + 1) + ":"
								+ (position + 1);
						newHeadsCounters[0] = newLeftHeadPosition;
						newHeadsCounters[1] = newLeftHeadPosition;
						newHeadsCounters[counterMapping[lastOccurrenceVariable] + 2] = i;

						if (confiVisited.get(confiToKey(newState,
								newHeadsCounters)) == null) 
						{
							confiVisited.put(confiToKey(newState,
									newHeadsCounters), 1);
							if (searchForFinalConfi(newState, newHeadsCounters,
									varOrder, occurrenceVector, word,
									confiVisited)) 
							{
								return true;
							}
						}
					}
				}
			}
			return false;
		case 4: // Finding State
			splittedState = state.split(":");
			int findVariable = Integer.valueOf(splittedState[1]);
			leftHeadPosition = Integer.valueOf(splittedState[2]);
			gap = gaps[leftHeadPosition];

			// Last occurrence reached, so a reset state has to be entered
			if (roMapping[findVariable] == leftHeadPosition) 
			{
				newState = "3:" + varOrder.get(leftHeadPosition);

				if (confiVisited.get(confiToKey(newState, headsCounters)) == null) 
				{
					confiVisited.put(confiToKey(newState, headsCounters), 1);
					if (searchForFinalConfi(newState, headsCounters, varOrder,
							occurrenceVector, word, confiVisited)) 
					{
						return true;
					}
				}
			}
			// move the right head
			else {
				// The gap is a forth gap, so a forth (>) state has to be
				// entered
				if (gap[0] < gap[1]) 
				{
					int numberOfSteps = 0;
					for (int i = gap[0]; i < gap[1]; i++) 
					{
						int counterIndex = counterMapping[varOrder.get(i)];
						numberOfSteps = numberOfSteps
								+ headsCounters[counterIndex + 2];
					}

					if (headsCounters[1] + numberOfSteps <= word.length()) 
					{
						newState = "2:" + findVariable + ":" + leftHeadPosition;
						headsCounters[1] = headsCounters[1] + numberOfSteps;

						if (confiVisited
								.get(confiToKey(newState, headsCounters)) == null) 
						{
							confiVisited.put(
									confiToKey(newState, headsCounters), 1);
							if (searchForFinalConfi(newState, headsCounters,
									varOrder, occurrenceVector, word,
									confiVisited)) 
							{
								return true;
							}
						}
					}

				}
				// The gap is a back gap, so a back (<) state has to be entered
				else if (gap[0] > gap[1]) 
				{
					int numberOfSteps = 0;
					for (int i = gap[1]; i < gap[0]; i++) 
					{
						int counterIndex = counterMapping[varOrder.get(i)];
						numberOfSteps = numberOfSteps
								+ headsCounters[counterIndex + 2];
					}

					if (headsCounters[1] - numberOfSteps > -1) 
					{
						newState = "2:" + findVariable + ":" + leftHeadPosition;
						headsCounters[1] = headsCounters[1] - numberOfSteps;

						if (confiVisited
								.get(confiToKey(newState, headsCounters)) == null) 
						{
							confiVisited.put(
									confiToKey(newState, headsCounters), 1);
							if (searchForFinalConfi(newState, headsCounters,
									varOrder, occurrenceVector, word,
									confiVisited)) 
							{
								return true;
							}
						}
					}
				}
				// The right head is already on the correct position so the next
				// matching can be performed
				else {
					newState = "2:" + findVariable + ":" + leftHeadPosition;

					if (confiVisited.get(confiToKey(newState, headsCounters)) == null) 
					{
						confiVisited
								.put(confiToKey(newState, headsCounters), 1);
						if (searchForFinalConfi(newState, headsCounters,
								varOrder, occurrenceVector, word, confiVisited)) 
						{
							return true;
						}
					}
				}
			}
			return false;
		}
		return false;
	}

	private boolean createInitialConfigurations(int wordLength,
			int[] occurrenceVector, ArrayList<Integer> varOrder, String word,
			Hashtable<String, Integer> confiVisited) 
	{
		return computeInitialCounterBounds(wordLength, occurrenceVector, 0,
				varOrder, word, confiVisited);
	}

	public boolean computeInitialCounterBounds(int wordLength,
			int[] occurrenceVector, int boundNumber,
			ArrayList<Integer> varOrder, String word,
			Hashtable<String, Integer> confiVisited) 
	{
		//In this function, all possible counter bounds are computed recursively
		
		if (wordLength == 0) 
		{
			//End of recursion
			
			// Every counter bound has to be 0
			for (int i = boundNumber; i < counterBounds.length; i++) 
			{
				counterBounds[i] = 0;
			}

			// create configuration
			int[] newHeadsCounters = new int[occurrenceVector.length + 2];
			String newState = "1";
			newHeadsCounters[0] = -1;
			newHeadsCounters[1] = -1;
			for (int j = 2; j < newHeadsCounters.length; j++) 
			{
				newHeadsCounters[j] = counterBounds[j - 2];
			}

			
			if (confiVisited.get(confiToKey(newState, newHeadsCounters)) == null) 
			{
				//If this configuration has not been visited yet, visit it 
				confiVisited.put(confiToKey(newState, newHeadsCounters), 1);
				if (searchForFinalConfi(newState, newHeadsCounters, varOrder,
						occurrenceVector, word, confiVisited)) 
				{
					return true;
				}
			}
		} 
		else if (boundNumber == counterBounds.length - 1) 
		{
			//End of recursion
			for (int i = 0; i <= Math.floor(wordLength
					/ occurrenceVector[boundNumber]); i++) 
			{
				if (interrupted) 
				{
					return false;
				}
				counterBounds[boundNumber] = i;

				// create configuration
				int[] newHeadsCounters = new int[occurrenceVector.length + 2];
				String newState = "1";
				newHeadsCounters[0] = -1;
				newHeadsCounters[1] = -1;
				for (int j = 2; j < newHeadsCounters.length; j++) 
				{
					newHeadsCounters[j] = counterBounds[j - 2];
				}

				if (confiVisited.get(confiToKey(newState, newHeadsCounters)) == null) 
				{
					//If this configuration has not been visited yet, visit it 
					confiVisited.put(confiToKey(newState, newHeadsCounters), 1);
					if (searchForFinalConfi(newState, newHeadsCounters,
							varOrder, occurrenceVector, word, confiVisited)) 
					{
						return true;
					}
				}
			}
		} 
		else 
		{
			// For every possible length for the first element
			for (int i = 0; i <= Math.floor(wordLength
					/ occurrenceVector[boundNumber]); i++) 
			{
				if (interrupted) 
				{
					return false;
				}
				// create shorter Occurrence Vector which will be passed to the
				// next recursive call
				int newWordLength = wordLength
						- (i * occurrenceVector[boundNumber]);
				counterBounds[boundNumber] = i;
				int oldboundNumber = boundNumber;
				boundNumber++;
				//continue with recursively computing the initial counter bounds 
				if (computeInitialCounterBounds(newWordLength,
						occurrenceVector, boundNumber, varOrder, word,
						confiVisited)) 
				{
					return true;
				}
			
				boundNumber = oldboundNumber;
			}
		}
		return false;
	}

	private int computeBoundForNewCounterBound(ArrayList<Integer> varOrder,
			int varDistance, String word, int leftHeadPosition,
			int patternPosition, int[] currentCounterBounds) 
	{
		int remainingWordLength = word.length() - leftHeadPosition;
		int[] variablesCurrentlyOccupyingCounter = new int[varDistance + 1];

		for (int i = 0; i < variablesCurrentlyOccupyingCounter.length; i++) 
		{
			variablesCurrentlyOccupyingCounter[i] = -1;
		}
		for (int i = 0; i < varOrder.size(); i++) 
		{
			if ((i < patternPosition)
					&& (roMapping[varOrder.get(i)] > patternPosition)) 
			{
				variablesCurrentlyOccupyingCounter[counterMapping[varOrder
						.get(i)]] = varOrder.get(i);
			}
			if ((i >= patternPosition)
					&& (variablesCurrentlyOccupyingCounter[counterMapping[varOrder
							.get(i)]] == -1)) 
			{
				variablesCurrentlyOccupyingCounter[counterMapping[varOrder
						.get(i)]] = varOrder.get(i);
			}
		}

		int nextVariableUsingCounter = -1;
		for (int i = patternPosition + 1; i < varOrder.size(); i++) 
		{
			if (counterMapping[varOrder.get(i)] == counterMapping[varOrder
					.get(patternPosition)]) 
			{
				nextVariableUsingCounter = varOrder.get(i);
				break;
			}
		}
		variablesCurrentlyOccupyingCounter[counterMapping[varOrder
				.get(patternPosition)]] = nextVariableUsingCounter;
		int[] OccurrenceNumbersOfOccupyingVariables = new int[varDistance + 1];
		for (int i = patternPosition; i < varOrder.size(); i++) 
		{
			if (varOrder.get(i) == variablesCurrentlyOccupyingCounter[counterMapping[varOrder
					.get(i)]]) {
				OccurrenceNumbersOfOccupyingVariables[counterMapping[varOrder
						.get(i)]]++;
			}
		}

		int boundForNewCounterBound = 0;
		// If there is still a variable left that will use this counter, compute
		// a counter bound bound.
		if (!(OccurrenceNumbersOfOccupyingVariables[counterMapping[varOrder
				.get(patternPosition)]] == 0)) 
		{
			for (int i = 0; i < varDistance + 1; i++) 
			{
				if (i != counterMapping[varOrder.get(patternPosition)]) 
				{
					boundForNewCounterBound = boundForNewCounterBound
							+ (OccurrenceNumbersOfOccupyingVariables[i] * currentCounterBounds[i + 2]);
				}
			}
			boundForNewCounterBound = remainingWordLength
					- boundForNewCounterBound;
			boundForNewCounterBound = (int) Math
					.floor(boundForNewCounterBound
							/ OccurrenceNumbersOfOccupyingVariables[counterMapping[varOrder
									.get(patternPosition)]]);
		}

		return boundForNewCounterBound;
	}

	String confiToKey(String state, int[] headsCounters) {
		String key = state;

		for (int i = 0; i < headsCounters.length; i++) {
			key = key + ":" + headsCounters[i];
		}

		return key;
	}

	public void run() 
	{
		isMember = solveInstance(pattern, word);
	}

}